The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
terms(X) → n__terms(X)
s(X) → n__s(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(X) → X

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of terms: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 0th argument of activate: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 0th argument of first: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 1th argument of first: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 0th argument of sqr: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 0th argument of s: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 0th argument of add: s, sqr, terms, add, dbl, first, activate
The following defined symbols can occur below the 1th argument of add: dbl

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
dbl(s(X)) → s(s(dbl(X)))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

dbl(0) → 0
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
terms(X) → n__terms(X)
terms(N) → cons(recip(sqr(N)), n__terms(n__s(N)))
first(0, X) → nil
activate(X) → X
sqr(0) → 0
add(0, X) → X
activate(n__s(X)) → s(activate(X))
activate(n__terms(X)) → terms(activate(X))
add(s(X), Y) → s(add(X, Y))
first(X1, X2) → n__first(X1, X2)
sqr(s(X)) → s(add(sqr(X), dbl(X)))
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
s(X) → n__s(X)

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

dbl(0) → 0 [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
first(0, X) → nil [1]
activate(X) → X [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(X1, X2) → n__first(X1, X2) [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
s(X) → n__s(X) [1]

Rewrite Strategy: INNERMOST

(5) InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID) transformation)

Removed the following rules with non-basic left-hand side, as they cannot be used in innermost rewriting:

first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1]
add(s(X), Y) → s(add(X, Y)) [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]

Due to the following rules that have to be used instead:

s(X) → n__s(X) [1]

(6) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

dbl(0) → 0 [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
first(0, X) → nil [1]
activate(X) → X [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
s(X) → n__s(X) [1]

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

dbl(0) → 0 [1]
terms(X) → n__terms(X) [1]
terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
first(0, X) → nil [1]
activate(X) → X [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
activate(n__s(X)) → s(activate(X)) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
s(X) → n__s(X) [1]

The TRS has the following type information:

dbl :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first 0 :: 0:n__terms:n__s:cons:nil:n__first terms :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first n__terms :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first cons :: recip → 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first recip :: 0:n__terms:n__s:cons:nil:n__first → recip sqr :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first n__s :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first first :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first nil :: 0:n__terms:n__s:cons:nil:n__first activate :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first add :: 0:n__terms:n__s:cons:nil:n__first → add → add s :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first n__first :: 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first → 0:n__terms:n__s:cons:nil:n__first

Rewrite Strategy: INNERMOST

(9) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

dbl
add

(c) The following functions are completely defined:

activate
terms
first
sqr
s

Due to the following rules being added:

sqr(v0) → null_sqr [0]

And the following fresh constants:

null_sqr, const, const1

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: dbl(0) → 0 [1] terms(X) → n__terms(X) [1] terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1] first(0, X) → nil [1] activate(X) → X [1] sqr(0) → 0 [1] add(0, X) → X [1] activate(n__s(X)) → s(activate(X)) [1] activate(n__terms(X)) → terms(activate(X)) [1] first(X1, X2) → n__first(X1, X2) [1] activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1] s(X) → n__s(X) [1] sqr(v0) → null_sqr [0] The TRS has the following type information: dbl :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr 0 :: 0:n__terms:n__s:cons:nil:n__first:null_sqr terms :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr n__terms :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr cons :: recip → 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr recip :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → recip sqr :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr n__s :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr first :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr nil :: 0:n__terms:n__s:cons:nil:n__first:null_sqr activate :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr add :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → add → add s :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr n__first :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr null_sqr :: 0:n__terms:n__s:cons:nil:n__first:null_sqr const :: recip const1 :: add Rewrite Strategy: INNERMOST

(11) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(12) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: dbl(0) → 0 [1] terms(X) → n__terms(X) [1] terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1] first(0, X) → nil [1] activate(X) → X [1] sqr(0) → 0 [1] add(0, X) → X [1] activate(n__s(X)) → s(X) [2] activate(n__s(n__s(X'))) → s(s(activate(X'))) [2] activate(n__s(n__terms(X''))) → s(terms(activate(X''))) [2] activate(n__s(n__first(X1', X2'))) → s(first(activate(X1'), activate(X2'))) [2] activate(n__terms(X)) → terms(X) [2] activate(n__terms(n__s(X3))) → terms(s(activate(X3))) [2] activate(n__terms(n__terms(X4))) → terms(terms(activate(X4))) [2] activate(n__terms(n__first(X1'', X2''))) → terms(first(activate(X1''), activate(X2''))) [2] first(X1, X2) → n__first(X1, X2) [1] activate(n__first(X1, X2)) → first(X1, X2) [3] activate(n__first(X1, n__s(X7))) → first(X1, s(activate(X7))) [3] activate(n__first(X1, n__terms(X8))) → first(X1, terms(activate(X8))) [3] activate(n__first(X1, n__first(X12, X22))) → first(X1, first(activate(X12), activate(X22))) [3] activate(n__first(n__s(X5), X2)) → first(s(activate(X5)), X2) [3] activate(n__first(n__s(X5), n__s(X9))) → first(s(activate(X5)), s(activate(X9))) [3] activate(n__first(n__s(X5), n__terms(X10))) → first(s(activate(X5)), terms(activate(X10))) [3] activate(n__first(n__s(X5), n__first(X13, X23))) → first(s(activate(X5)), first(activate(X13), activate(X23))) [3] activate(n__first(n__terms(X6), X2)) → first(terms(activate(X6)), X2) [3] activate(n__first(n__terms(X6), n__s(X14))) → first(terms(activate(X6)), s(activate(X14))) [3] activate(n__first(n__terms(X6), n__terms(X15))) → first(terms(activate(X6)), terms(activate(X15))) [3] activate(n__first(n__terms(X6), n__first(X16, X24))) → first(terms(activate(X6)), first(activate(X16), activate(X24))) [3] activate(n__first(n__first(X11, X21), X2)) → first(first(activate(X11), activate(X21)), X2) [3] activate(n__first(n__first(X11, X21), n__s(X17))) → first(first(activate(X11), activate(X21)), s(activate(X17))) [3] activate(n__first(n__first(X11, X21), n__terms(X18))) → first(first(activate(X11), activate(X21)), terms(activate(X18))) [3] activate(n__first(n__first(X11, X21), n__first(X19, X25))) → first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) [3] s(X) → n__s(X) [1] sqr(v0) → null_sqr [0] The TRS has the following type information: dbl :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr 0 :: 0:n__terms:n__s:cons:nil:n__first:null_sqr terms :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr n__terms :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr cons :: recip → 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr recip :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → recip sqr :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr n__s :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr first :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr nil :: 0:n__terms:n__s:cons:nil:n__first:null_sqr activate :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr add :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → add → add s :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr n__first :: 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr → 0:n__terms:n__s:cons:nil:n__first:null_sqr null_sqr :: 0:n__terms:n__s:cons:nil:n__first:null_sqr const :: recip const1 :: add Rewrite Strategy: INNERMOST

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 1
null_sqr => 0
const => 0
const1 => 0

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ terms(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ terms(terms(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ terms(s(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ s(terms(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = N, N >= 0

(15) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = N, N >= 0

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ terms(terms(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ terms(s(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = 1 + X, X >= 0, X = N, N >= 0
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + N)) :|: z = N, N >= 0, N = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + N)) :|: z = N, N >= 0, v0 >= 0, N = v0

(17) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ first } { dbl } { add } { terms } { sqr } { s } { activate }

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {add}, {terms}, {sqr}, {s}, {activate}

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: ?, size: O(n1) [1 + z + z']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z']

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z']

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: ?, size: O(1) [0]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0]

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: ?, size: O(n1) [z']

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z']

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z']

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 4 + z

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: ?, size: O(n1) [4 + z]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z]

(43) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(44) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z]

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(46) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: ?, size: O(1) [0]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(48) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0]

(49) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(50) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0]

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(52) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0] s: runtime: ?, size: O(n1) [1 + z]

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(54) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z]

(55) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(56) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z]

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 92 + 195·z + 22·z²

(58) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: ?, size: O(n2) [92 + 195·z + 22·z2]

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 132 + 264·z

(60) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ s(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(first(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 3 }→ first(X1, terms(activate(X8))) :|: X1 >= 0, z = 1 + X1 + (1 + X8), X8 >= 0
activate(z) -{ 3 }→ first(X1, s(activate(X7))) :|: z = 1 + X1 + (1 + X7), X1 >= 0, X7 >= 0
activate(z) -{ 3 }→ first(X1, first(activate(X12), activate(X22))) :|: X1 >= 0, X12 >= 0, X22 >= 0, z = 1 + X1 + (1 + X12 + X22)
activate(z) -{ 3 }→ first(terms(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), terms(activate(X15))) :|: X6 >= 0, z = 1 + (1 + X6) + (1 + X15), X15 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), s(activate(X14))) :|: z = 1 + (1 + X6) + (1 + X14), X6 >= 0, X14 >= 0
activate(z) -{ 3 }→ first(terms(activate(X6)), first(activate(X16), activate(X24))) :|: X16 >= 0, z = 1 + (1 + X6) + (1 + X16 + X24), X6 >= 0, X24 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 3 }→ first(s(activate(X5)), terms(activate(X10))) :|: X5 >= 0, X10 >= 0, z = 1 + (1 + X5) + (1 + X10)
activate(z) -{ 3 }→ first(s(activate(X5)), s(activate(X9))) :|: X5 >= 0, X9 >= 0, z = 1 + (1 + X5) + (1 + X9)
activate(z) -{ 3 }→ first(s(activate(X5)), first(activate(X13), activate(X23))) :|: X5 >= 0, z = 1 + (1 + X5) + (1 + X13 + X23), X13 >= 0, X23 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), terms(activate(X18))) :|: z = 1 + (1 + X11 + X21) + (1 + X18), X11 >= 0, X21 >= 0, X18 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), s(activate(X17))) :|: z = 1 + (1 + X11 + X21) + (1 + X17), X11 >= 0, X21 >= 0, X17 >= 0
activate(z) -{ 3 }→ first(first(activate(X11), activate(X21)), first(activate(X19), activate(X25))) :|: X11 >= 0, X21 >= 0, X19 >= 0, X25 >= 0, z = 1 + (1 + X11 + X21) + (1 + X19 + X25)
activate(z) -{ 4 }→ 1 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X2 = X, X >= 0, X1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
activate(z) -{ 4 }→ 1 + (1 + s) + (1 + (1 + N)) :|: s >= 0, s <= 0, z - 1 >= 0, z - 1 = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
dbl(z) -{ 1 }→ 0 :|: z = 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 0 }→ 0 :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 1 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed:
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [1 + z + z'] dbl: runtime: O(1) [1], size: O(1) [0] add: runtime: O(1) [1], size: O(n1) [z'] terms: runtime: O(1) [2], size: O(n1) [4 + z] sqr: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [132 + 264·z], size: O(n2) [92 + 195·z + 22·z2]

(61) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(62) BOUNDS(1, n^1)